Date: Wed, 20 Nov 1996 19:14:45 GMT
Server: Apache/1.0.3
Content-type: text/html
Content-length: 2389
Last-modified: Wed, 15 May 1996 16:33:38 GMT

<html>
<HEAD><TITLE> Digital Design Derivation </TITLE></HEAD>
<H2> Digital Design Derivation </H2>



<Strong>Description: </Strong> 
<Blockquote>
This research adapts a formal programming methodology to the construction of
 digital systems.
An algebra for manipulating modeling expressions is used to reduce
 higher-level specifications of behavior to structures mapping directly
 into VLSI technologies.
This work links a large body of research in program refinement---to
 which this department has been a significant contributor---with
 other formal methods as applied to digital design.

A principal goal of this research has been to establish
 algebraic derivation as a mode of <em>formal verification</em>.
The tendency in <em> formal methods research </em> toward deductive proofs
 of correctness does not reflect design practice.
Our central thesis is that effective automated reasoning in design
 must provide well-integrated support of a variety of reasoning systems.
Hence, a task of this project is to develop an algebraic formalism that is
 on a par, mathematically and mechanically, with contemporary deductive systems.
A large component of our research activity has to do with the the
 implementation of the DDD algebra, its integration with CAD tools and other
 formal systems, and the application these tools to realistic design problems.
</Blockquote>
<P>

<Strong> Associated Faculty: </Strong>  
<UL>
<LI>
   <!WA0><A href="http://www.cs.indiana.edu/people/s/sjohnson.html">
   Steven D. Johnson </A>
</UL>
<P>

<Strong> Associated Graduate Students: </Strong>  
<!WA1><A href="http://www.cs.indiana.edu/hyplan/bose.html">
  Bhaskar Bose (PhD 1994)</A>,
<!WA2><A href="http://www.cs.indiana.edu/hyplan/kfisler.html">
  Kathi Fisler</A>,
<!WA3><A href="http://atb-www.larc.nasa.gov/~psm/bio-psm.html">
  Paul Miner </A>,
<!WA4><A href="http://www.cs.indiana.edu/people/r/rathk.html">
  Kamlesh Rath (PhD 1995)</A>,
<!WA5><A href="http://www.cs.indiana.edu/hyplan/mtuna.html">
  M. Esen Tuna<\A>. 
Zheng Zhu (PhD 1992),
<P>


<Strong> Support: </Strong> 
Supported by NSF under grants
MIP87-07067 (1987--89), MIP89-21842 (1989--92), MIP92-08745 (1992--95),
with infrastructure support from DCR85-52598 and CDA93-03189.
<p> 

<Strong> For more information </Strong> <em> Coming Soon </em>
<p>

<!WA6><a href="http://www.cs.indiana.edu/l/www/research/index.html"><!WA7><IMG SRC="http://www.cs.indiana.edu/research/back.gif">Return to Computer Science Research Page</a>








